the_w:World, e, e':E. (e = e')  (e = e') 

latex

Definitions	x:A. B(x), P  Q, P & Q, P  Q, P  Q, t  T, , p = q, t.1, t.2, E,
Lemmas	assert-w-eq-E, assert wf, w-eq-E wf, w-E wf, world wf, iff transitivity, band wf, eq id wf, eq int wf, Id wf, assert of band, and functionality wrt iff, assert-eq-id, assert of eq int